k:Knd, T, A, B:Type, l:IdLnk, x, tg:Id, f:(ABT), c:(AB).
((isrcv(k))  (destination(lnk(k)) = source(l)  Id & ((lnk(k) = l)  (T = B & tag(k) = tg))))
 Normal(A)
 Normal(T)
 Normal(B)
 es. k(v:B) sends
 es. kf(x:A,v) on
 es. kl tagged with tg:T
 es. kprovided c(x,v) 

latex

Definitions	outl(x), t.1, True, tt, {T}, SQType(T), rcv(l,tg), x. t(x), , t  T, if b then t else f fi , lnk(k), P & Q, b, P  Q, x:A. B(x), x(s), Normal(T)
Lemmas	bool wf, tagof wf, IdLnk wf, lsrc wf, lnk wf, ldst wf, Id wf, isrcv wf, normal-type wf, assert wf, rcv wf, Knd wf, Knd sq, sends1-p-realizable, conditional-send1-p wf, event system wf, ifthenelse wf, sends1-p wf, es-real-monotonicity, sends1-p-implies-conditional-send1-p